f3(0, 1, x) -> f3(s1(x), x, x)
f3(x, y, s1(z)) -> s1(f3(0, 1, z))
↳ QTRS
↳ DependencyPairsProof
f3(0, 1, x) -> f3(s1(x), x, x)
f3(x, y, s1(z)) -> s1(f3(0, 1, z))
F3(x, y, s1(z)) -> F3(0, 1, z)
F3(0, 1, x) -> F3(s1(x), x, x)
f3(0, 1, x) -> f3(s1(x), x, x)
f3(x, y, s1(z)) -> s1(f3(0, 1, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F3(x, y, s1(z)) -> F3(0, 1, z)
F3(0, 1, x) -> F3(s1(x), x, x)
f3(0, 1, x) -> f3(s1(x), x, x)
f3(x, y, s1(z)) -> s1(f3(0, 1, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F3(x, y, s1(z)) -> F3(0, 1, z)
Used ordering: Polynomial Order [17,21] with Interpretation:
F3(0, 1, x) -> F3(s1(x), x, x)
POL( 1 ) = 0
POL( 0 ) = max{0, -2}
POL( s1(x1) ) = x1 + 1
POL( F3(x1, ..., x3) ) = 2x3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
F3(0, 1, x) -> F3(s1(x), x, x)
f3(0, 1, x) -> f3(s1(x), x, x)
f3(x, y, s1(z)) -> s1(f3(0, 1, z))